es:ES, x, i:Id, T:Type.
(x, y:T. Dec(x = y  T))
 vartype(i;x)  T
 e'@i.
 (e<e'. (x when e) = (x when e')  T)
  (e:E.
  ((e <loc e')
  (& (x when e) = (x after e)  T
  (& & (e'':E. (e <loc e'')  e''  e'   (x when e'') = (x when e')  T)) 

latex

Definitions	x:A. B(x), P  Q, e@i. P(e), P  Q, x:A. B(x), A & B, P & Q, Prop, t  T, x. t(x), (e <loc e'), P  Q, x(s), P  Q
Lemmas	alle-at-iff, alle-lt wf, es-when wf, es-vartype wf, es-E wf, Id wf, es-loc wf, es-locl wf, not wf, es-loc-pred, es-locl-iff, es-after wf, es-le wf, es-le-loc, assert wf, es-first wf, es-pred wf, decidable wf, event system wf